Nuprl Lemma : compat_symmetry
0,22
postcript
pdf
T
:Type,
as
,
bs
:
T
List.
as
||
bs
bs
||
as
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
l1
l2
,
P
Q
,
{
T
}
,
Prop
,
P
Q
,
P
Q
,
P
&
Q
,
P
Q
,
l1
||
l2
Lemmas
iseg
wf
origin
T:Type, as, bs:T List. as || bs 
bs || as T:Type, as, bs:T List. as || bs bs || as 
Tx:A. B(x)
l2
Q
Q Q Q